#include <iostream>
#include "PDTCloneTraversal.h"
#include "PDTCodeGraph.h"

#include "PDTNumVar.h"
#include "PDTExpBoolBinNumDerived.h"
#include "PDTExpNumBinDerived.h"
#include "PDTProp.h"
#include "PDTNumConst.h"
#include "PDTAssign.h"
#include "PDTBoolVar.h"
#include "PDTExpBoolBinBoolDerived.h"
#include "PDTSetOp.h"
#include "PDTIfElse.h"
#include "PDTAssert.h"
#include "PDTListOfStatements.h"
#include "PDTType.h"
#include "PDTSetVar.h"
#include "PDTQuantifier.h"
#include "PDTBoolConst.h"
#include "PDTNeg.h"
#include "PDTNot.h"
#include "PDTWhile.h"
#include "PDTFunction.h"

PDTCloneTraversal :: PDTCloneTraversal(PDTCodeGraph & aCG, PDTNode *aTop)
    : cg(aCG), size(cg.nodes.size()), topNode(aTop)
{
    clones = new PDTNode *[size];
    for (unsigned int i = 0; i < size; i++)
        clones[i] = NULL;
}

PDTCloneTraversal :: ~PDTCloneTraversal() {
    for (unsigned int i = 0; i < size; i++)
        delete clones[i];
    delete [] clones;
}

bool 
PDTCloneTraversal :: setClone(PDTNode & d, PDTNode * clone) {
    unsigned int idx = d.getId();
    clones[idx] = clone;
    return true;
}

bool 
PDTCloneTraversal :: isTopNode(PDTNode * node) const {
    return node == topNode;
}

PDTNode * 
PDTCloneTraversal :: getChildClone(PDTNode & d, unsigned int i) const {
    vector<PDTNode * > & children = d.getChildren();
    PDTNode * child = children[i];
    PDTNode * clone = getClone(*child);
    return clone;
}

PDTNode * 
PDTCloneTraversal :: getClone(PDTNode & d) const {
    unsigned int id = d.getId();
    return clones[id];
}

PDTNode * 
PDTCloneTraversal :: getClone(PDTNode * d) const {
    return getClone(*d);
}

#define CLONE_BINARY_OP_LR(CLS_NAME, LEFT_OP_TYPE, RIGHT_OP_TYPE) \
    LEFT_OP_TYPE * lft = (LEFT_OP_TYPE*) getChildClone(d, 0); \
    if (lft == NULL) return Traversal::Stop; \
    RIGHT_OP_TYPE * rgt = (RIGHT_OP_TYPE*) getChildClone(d, 1); \
    if (rgt == NULL) return Traversal::Stop; \
    PDTNode * clone = new CLS_NAME(cg, *lft, *rgt); \
    if (clone == NULL) return Traversal::Stop; \
    setClone(d,clone); \
    return  Traversal::Continue;


#define CLONE_BINARY_OP(CLS_NAME, OPERAND_TYPE) \
        CLONE_BINARY_OP_LR(CLS_NAME, OPERAND_TYPE, OPERAND_TYPE)


#define CLONE_UNARY_OP(CLS_NAME, OP_TYPE) \
    PDTNode* cClone = getChildClone(d,0); \
    OP_TYPE* expClone = dynamic_cast<OP_TYPE*>(cClone); \
    if (expClone == NULL) \
        return Traversal::Stop; \
    CLS_NAME * clone = new CLS_NAME(cg, *expClone); \
    if (clone == NULL) \
        return Traversal::Stop; \
    setClone(d,clone); \
    return Traversal::Continue;

#define CLONE_CONST() \
    if (getClone(d) == NULL) \
         setClone(d,&d); \
    return Traversal::Continue;

#define NOT_IMPLEMENTED_YET \
    olog() << "Not implemented yet!" << endl;

#define CLONE_VAR(CLS_NAME) \
    if (getClone(d) != NULL) \
        return Traversal::Continue; \
    PDTFunctionDec * funcDec = d.getFunctionDec(); \
    if (! isTopNode((PDTNode*)funcDec)) { \
        setClone(d,&d); \
        return Traversal::Continue; \
    } \
    const string & name = d.getName(); \
    CLS_NAME * clone = new CLS_NAME(cg, name); \
    if(clone == NULL) \
        return Traversal::Stop; \
    setClone(d,clone); \
    return Traversal::Continue;

#define CLONE_SEQ_VAR(CLS_NAME,Seq) \
    if (getClone(d) != NULL) \
        return Traversal::Continue; \
    PDTFunctionDec * funcDec = d.getFunctionDec(); \
    if (! isTopNode((PDTNode*)funcDec)) { \
        setClone(d,&d); \
        return Traversal::Continue; \
    } \
    const string & name = d.getName(); \
    CLS_NAME * clone = new CLS_NAME(cg, *Seq, name); \
    if(clone == NULL) \
        return Traversal::Stop; \
    setClone(d,clone); \
    return Traversal::Continue;

#define CLONE_QUANTIFIER(Q_TYPE) \
    unsigned int i = 0; \
    vector <PDTVar *> vars; \
    for (; i < d.getNumVars(); i++) { \
        PDTNode * clone = getChildClone(d,i); \
        if (clone == NULL) \
            return Traversal::Stop; \
        PDTVar * vClone = dynamic_cast<PDTVar *>(clone); \
        vars.push_back(vClone); \
    } \
    PDTNode* nodeClone = getChildClone(d,i); \
    PDTExpBool * expClone = dynamic_cast<PDTExpBool*>(nodeClone); \
    if (expClone == NULL) \
        return Traversal::Stop; \
    Q_TYPE * clone = new Q_TYPE(cg, vars, *expClone); \
    if (clone == NULL)  \
        return Traversal::Stop; \
    setClone(d,clone); \
    return Traversal::Continue;


// PDTAdd 
Traversal::RetType PDTCloneTraversal :: post(PDTAdd & d) {
    CLONE_BINARY_OP(PDTAdd,PDTExpNum)
}


// PDTAnd 
Traversal::RetType PDTCloneTraversal :: post(PDTAnd & d) {
    CLONE_BINARY_OP(PDTAnd,PDTExpBool)
}


// PDTAssert 
Traversal::RetType PDTCloneTraversal :: post(PDTAssert & d) {
    NOT_IMPLEMENTED_YET
    return Traversal::Continue;
}


// PDTAssign 
Traversal::RetType PDTCloneTraversal :: post(PDTAssign & d) {
    CLONE_BINARY_OP_LR(PDTAssign,PDTVar,PDTExp)
}


// PDTBehavior 
Traversal::RetType PDTCloneTraversal :: post(PDTBehavior & d) {
    NOT_IMPLEMENTED_YET
    return Traversal::Continue;
}


// PDTBehaviors 
Traversal::RetType PDTCloneTraversal :: post(PDTBehaviors & d) {
    NOT_IMPLEMENTED_YET
    return Traversal::Continue;
}


// PDTBoolConst 
Traversal::RetType PDTCloneTraversal :: post(PDTBoolConst & d) {
    CLONE_CONST()
    return Traversal::Continue;
}


// PDTBoolVar 
Traversal::RetType PDTCloneTraversal :: post(PDTBoolVar & d) {
    CLONE_VAR(PDTBoolVar)
}

// PDTConstSequence 
Traversal::RetType PDTCloneTraversal :: post(PDTConstSequence & d) {
    CLONE_CONST()
    return Traversal::Continue;
}


// PDTDiv 
Traversal::RetType PDTCloneTraversal :: post(PDTDiv & d) {
    CLONE_BINARY_OP(PDTDiv,PDTExpNum)
}


// PDTEqualBool 
Traversal::RetType PDTCloneTraversal :: post(PDTEqualBool & d) {
    CLONE_BINARY_OP(PDTEqualBool,PDTExpBool)
}


// PDTEqualNum 
Traversal::RetType PDTCloneTraversal :: post(PDTEqualNum & d) {
    CLONE_BINARY_OP(PDTEqualNum,PDTExpNum)
}


// PDTExist 
Traversal::RetType PDTCloneTraversal :: post(PDTExist & d) {
    CLONE_QUANTIFIER(PDTExist)
}


// PDTForall 
Traversal::RetType PDTCloneTraversal :: post(PDTForall & d) {
    CLONE_QUANTIFIER(PDTForall)
}


// PDTFunctionCall 
Traversal::RetType PDTCloneTraversal :: post(PDTFunctionCall & d) {
    unsigned int i = 0; 
    vector <PDTNode *> args; 
    for (; i < d.getArgumentCount(); i++) {
        PDTNode * clone = getChildClone(d,i); 
        if (clone == NULL)
            return Traversal::Stop;
        args.push_back(clone); 
    } 
    //TODO: check what happens to the return var!

    PDTFunctionDec * funcPtr = d.getFuncPtr();
    PDTNode * funcClone = getClone(funcPtr);
    PDTFunctionDec * funcDecClone = dynamic_cast<PDTFunctionDec*>(funcClone);
    if (funcDecClone == NULL)
        return Traversal::Stop;

    string name = d.getName();
    PDTFunctionCall * clone = new PDTFunctionCall(cg, args, name, funcDecClone);
    if (clone == NULL)
        return Traversal::Stop;
    setClone(d,clone);
    return Traversal::Continue;
}


// PDTFunctionDec 
Traversal::RetType PDTCloneTraversal :: post(PDTFunctionDec & d) {
    if (getClone(d) != NULL)
        return Traversal::Continue;

    unsigned int i = 0; 
    vector <PDTVar *> args; 
    for (; i < d.getArgumentCount(); i++) {
        PDTNode * clone = getChildClone(d,i); 
        PDTVar * vClone = dynamic_cast<PDTVar *>(clone);
        if (vClone == NULL)
            return Traversal::Stop;
        args.push_back(vClone);
    } 
    PDTVar * retVar  = d.getReturnVar();
    PDTNode * retNode = retVar->getNode();
    PDTNode * retClone = getClone(*retNode);
    PDTVar * retVarClone = dynamic_cast<PDTVar*>(retClone);
    if (retVarClone == NULL)
        return Traversal::Stop;

    PDTListOfStatements* list = d.getStatements();
    PDTNode * listNodeClone = getClone(*list);
    PDTListOfStatements* listClone = dynamic_cast<PDTListOfStatements*>(listNodeClone);
    if (listClone == NULL) 
        return Traversal::Stop;

    string name = d.getName();

    PDTFunctionDec * clone = new PDTFunctionDec(cg, name,*listClone, retVarClone, args);

    if (clone == NULL)
        return Traversal::Stop;
    setClone(d,clone);
    return Traversal::Continue;
}

// PDTGreaterThan 
Traversal::RetType PDTCloneTraversal :: post(PDTGreaterThan & d) {
    CLONE_BINARY_OP(PDTGreaterThan,PDTExpNum)
}


// PDTGreaterThanEqual 
Traversal::RetType PDTCloneTraversal :: post(PDTGreaterThanEqual & d) {
    CLONE_BINARY_OP(PDTGreaterThanEqual,PDTExpNum)
}


// PDTIfElse 
Traversal::RetType PDTCloneTraversal :: post(PDTIfElse & d) {
    PDTExpBool* cond = d.getCondition();
    PDTExpBool* condClone = dynamic_cast<PDTExpBool*>(getClone(cond));
    if (condClone == NULL)
        return Traversal::Stop;

    PDTStatement* ifStatement = d.getIfResult();
    PDTStatement* ifClone = dynamic_cast<PDTStatement*>(getClone(*ifStatement));
    if (ifClone == NULL)
        return Traversal::Stop;

    PDTStatement* elseStatement = d.getElseResult();
    PDTStatement* elseClone = dynamic_cast<PDTStatement*>(getClone(*elseStatement));
    if (elseClone == NULL)
        return Traversal::Stop;

    PDTIfElse * clone = new PDTIfElse(cg, *condClone, *ifClone, *elseClone);
    if (clone == NULL) 
        return Traversal::Stop;
    setClone(d,clone);
    return Traversal::Continue;
}


// PDTImplies 
Traversal::RetType PDTCloneTraversal :: post(PDTImplies & d) {
    CLONE_BINARY_OP(PDTImplies,PDTExpBool)
}


// PDTIntRange 
Traversal::RetType PDTCloneTraversal :: post(PDTIntRange & d) {
    NOT_IMPLEMENTED_YET
    return Traversal::Continue;
}


// PDTInvariant 
Traversal::RetType PDTCloneTraversal :: post(PDTInvariant & d) {
    NOT_IMPLEMENTED_YET
    return Traversal::Continue;
}


// PDTLessThan 
Traversal::RetType PDTCloneTraversal :: post(PDTLessThan & d) {
    CLONE_BINARY_OP(PDTLessThan,PDTExpNum)
}


// PDTLessThanEqual 
Traversal::RetType PDTCloneTraversal :: post(PDTLessThanEqual & d) {
    CLONE_BINARY_OP(PDTLessThanEqual,PDTExpNum)
}


// PDTListOfStatements 
Traversal::RetType PDTCloneTraversal :: post(PDTListOfStatements & d) {
    vector<PDTStatement*> statements;
    for (unsigned int i=0; i<d.numberOfStmts(); i++){
        PDTNode * clone = getChildClone(d,i);
        PDTStatement * statement = dynamic_cast<PDTStatement*>(clone);
        if (statement == NULL)
            return Traversal::Stop;
        statements.push_back(statement);
    }
    PDTListOfStatements * clone = new PDTListOfStatements(cg, statements);
    if (clone == NULL)
        return Traversal::Stop;
    setClone(d,clone);
    return Traversal::Continue;
}

// PDTMod 
Traversal::RetType PDTCloneTraversal :: post(PDTMod & d) {
    CLONE_BINARY_OP(PDTMod,PDTExpNum)
}


// PDTMult 
Traversal::RetType PDTCloneTraversal :: post(PDTMult & d) {
    CLONE_BINARY_OP(PDTMult,PDTExpNum)
}

// PDTNeg 
Traversal::RetType PDTCloneTraversal :: post(PDTNeg & d) {
    CLONE_UNARY_OP(PDTNeg, PDTExpNum) 
}


// PDTNilStatement 
Traversal::RetType PDTCloneTraversal :: post(PDTNilStatement & d) {
    if(getClone(d) == NULL)
        setClone(d,&d);
    return Traversal::Continue;
}


// PDTNot 
Traversal::RetType PDTCloneTraversal :: post(PDTNot & d) {
    CLONE_UNARY_OP(PDTNot, PDTExpBool) 
}


// PDTNotEqualBool 
Traversal::RetType PDTCloneTraversal :: post(PDTNotEqualBool & d) {
    CLONE_BINARY_OP(PDTNotEqualBool,PDTExpBool)
}


// PDTNotEqualNum 
Traversal::RetType PDTCloneTraversal :: post(PDTNotEqualNum & d) {
    CLONE_BINARY_OP(PDTNotEqualNum,PDTExpNum)
}


// PDTNumConst 
Traversal::RetType PDTCloneTraversal :: post(PDTNumConst & d) {
    CLONE_CONST()
}


// PDTNumConstDbl 
Traversal::RetType PDTCloneTraversal :: post(PDTNumConstDbl & d) {
    CLONE_CONST()
}


// PDTNumConstInt 
Traversal::RetType PDTCloneTraversal :: post(PDTNumConstInt & d) {
    CLONE_CONST()
}


// PDTNumVar 
Traversal::RetType PDTCloneTraversal :: post(PDTNumVar & d) {
    CLONE_VAR(PDTNumVar)
}


// PDTOr 
Traversal::RetType PDTCloneTraversal :: post(PDTOr & d) {
    CLONE_BINARY_OP(PDTOr,PDTExpBool)
}


// PDTPair 
Traversal::RetType PDTCloneTraversal :: post(PDTPair & d) {
    NOT_IMPLEMENTED_YET
    return Traversal::Continue;
}


// PDTPostCondition 
Traversal::RetType PDTCloneTraversal :: post(PDTPostCondition & d) {
    NOT_IMPLEMENTED_YET
    return Traversal::Continue;
}


// PDTPreCondition 
Traversal::RetType PDTCloneTraversal :: post(PDTPreCondition & d) {
    NOT_IMPLEMENTED_YET
    return Traversal::Continue;
}


// PDTProp 
Traversal::RetType PDTCloneTraversal :: post(PDTProp & d) {
    NOT_IMPLEMENTED_YET
    return Traversal::Continue;
}


// PDTRelation 
Traversal::RetType PDTCloneTraversal :: post(PDTRelation & d) {
    NOT_IMPLEMENTED_YET
    return Traversal::Continue;
}


// PDTSequence 
Traversal::RetType PDTCloneTraversal :: post(PDTSequence & d) {
    CLONE_CONST()
    return Traversal::Continue;
}


// PDTSequenceAccessBool 
Traversal::RetType PDTCloneTraversal :: post(PDTSequenceAccessBool & d) {
    CLONE_BINARY_OP_LR(PDTSequenceAccessBool,PDTSequenceVar,PDTExpNum)
}


// PDTSequenceAccessNum 
Traversal::RetType PDTCloneTraversal :: post(PDTSequenceAccessNum & d) {
    CLONE_BINARY_OP_LR(PDTSequenceAccessNum,PDTSequenceVar,PDTExpNum)
}


// PDTSequenceAssign 
Traversal::RetType PDTCloneTraversal :: post(PDTSequenceAssign & d) {
    NOT_IMPLEMENTED_YET
    return Traversal::Continue;
}


// PDTSequenceVar 
Traversal::RetType PDTCloneTraversal :: post(PDTSequenceVar & d) {
    PDTSequence * seq = d.getSequence();
    PDTSequence * cloneSeq = dynamic_cast<PDTSequence*>(getClone(seq));
    if (cloneSeq == NULL) {
	olog() << "sending Stop flag!" << endl;
        return Traversal::Stop;
    }
    CLONE_SEQ_VAR(PDTSequenceVar,seq)
}


// PDTSet 
Traversal::RetType PDTCloneTraversal :: post(PDTSet & d) {
    NOT_IMPLEMENTED_YET
    return Traversal::Continue;
}


// PDTSetVar 
Traversal::RetType PDTCloneTraversal :: post(PDTSetVar & d) {
    NOT_IMPLEMENTED_YET
    return Traversal::Continue;
}


// PDTSubt 
Traversal::RetType PDTCloneTraversal :: post(PDTSubt & d) {
    CLONE_BINARY_OP(PDTSubt,PDTExpNum)
}


// PDTWhile 
Traversal::RetType PDTCloneTraversal :: post(PDTWhile & d) {
    PDTExpBool* cond = d.getCondition();
    PDTNode * condClone = getClone(cond);
    PDTExpBool* condExpClone = dynamic_cast<PDTExpBool*>(condClone);
    if (condExpClone == NULL)
        return Traversal::Stop;

    PDTStatement* loop = d.getLoopStatement();
    PDTNode * loopClone = getClone(loop);
    PDTStatement * loopStatementClone = dynamic_cast<PDTStatement*>(loopClone);
    if (loopStatementClone == NULL)
        return Traversal::Stop;

    PDTWhile * clone = new PDTWhile(cg, *condExpClone, *loopStatementClone);
    if (clone == NULL)
        return Traversal::Stop;
    setClone(d,clone);
    return Traversal::Continue;
}

// PDTXor 
Traversal::RetType PDTCloneTraversal :: post(PDTXor & d) {
    CLONE_BINARY_OP(PDTXor,PDTExpBool)
}


// PDTUnresolvedExp 
Traversal::RetType PDTCloneTraversal :: post(PDTUnresolvedExp & d) {
    CLONE_CONST()
}


// PDTType 
Traversal::RetType PDTCloneTraversal :: post(PDTType & d) {
    CLONE_CONST()
}


// PDTUnaryNumExpr 
Traversal::RetType PDTCloneTraversal :: post(PDTUnaryNumExpr & d) {
    PDTUnaryOp & op = d.isMinus()? 
        PDTUnaryOp::PDTUnaryMinus :
        PDTUnaryOp::PDTUnaryPlus;

    PDTNode* cClone = getChildClone(d,0); 
    PDTExpNum* expClone = dynamic_cast<PDTExpNum*>(cClone); 
    if (expClone == NULL) 
        return Traversal::Stop; 
    PDTUnaryNumExpr* clone = new PDTUnaryNumExpr(cg, op, *expClone);
    if (clone == NULL)
        return Traversal::Stop;
    setClone(d,clone);
    return Traversal::Continue;
}
